COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDVAR x y z s
C00004 ENDMK
C⊗;
declare INDVAR x y z s;

declare INDCONST I, S0, desk, home,car,airport,county;

declare PREDCONST at 3, walkable 2, drivable 2;

declare OPCONST walk 2, drive 2;

axiom walkable:	walkable(home,S0);;

axiom drivable:	drivable(county,S0);;

axiom at:
	at(I,desk,S0)
	at(desk,home,S0)
	at(car,home,S0)
	at(home,county,S0)
	at(airport,county,S0)
;;

axiom attrans:
	∀x y z s.(at(x,y,s) ∧ at(y,z,s) ⊃ at(x,z,s))
;;

axiom walk:
	∀x y z s.((walkable(x,s) ∧ at(y,x,s) ∧ at(z,x,s) ∧ at(I,y,s))
		⊃ (at(I,z,walk(z,s))
		   ∧ ∀x.(walkable(x,walk(z,s)) ≡ walkable(x,s))
		   ∧ ∀x.(drivable(x,walk(z,s)) ≡ drivable(x,s))
		   ∧ ∀x y.(¬(x = I) ⊃ (at(x,y,walk(z,s)) ≡ at(x,y,s)))))
;;

axiom drive:
	∀x y z s.((drivable(x,s) ∧ at(y,x,s) 
				∧ at(z,x,s) ∧ at(car,y,s) ∧ at(I,car,s))
		⊃ (at(car,z,drive(z,s))
			∧ ∀x.(walkable(x,drive(z,s)) ≡ walkable(x,s))
			∧ ∀x.(drivable(x,drive(z,s)) ≡ drivable(x,s))
			∧ ∀x y.(¬(x = car ∨ at(x,car,s)) ∨ y=car
					 ⊃ (at(x,y,drive(z,s)) ≡ at(x,y,s)))))
;;

axiom notI:	¬(I=desk) ∧ ¬(I=car) ∧ ¬(I=home) ∧ ¬(I=airport);;